Section: New Results

Integration of formal methods in programming languages

Formal islands and Tom

Participants : Jean-Christophe Bach, Horatiu Cirstea, Pierre-Etienne Moreau, Claudia Tavares.

In [1] we have proposed a framework which makes possible the integration of formally defined constructs into an existing language. The Tom system is an instance of this principle: terms, first-order signatures, rewrite rules, strategies and matching constructs are integrated into Java and C for instance. The high level programming features provided by this approach are presented in  [48] . The Tom system is documented in  [27] . A general overview of the research problem raised by this approach are presented in  [47] .

One interest of Tom is to make the compilation process independent of the considered data-structure. Given any existing data-structure, using a formal anchor definition, it becomes possible to match and to apply transformation rules on the considered data-structures.

During the internship of Maxime Gabut, we have developed a new approach for parsing island based languages. We have clearly separated the grammars of the two considered languages (host and island languages). At present, there is one scanner for each language, but this is not powerful enough to handle the general case. We are currently studying another approach based on a scanner able to recognized tokens from both languages.

During the internship of Alexandre Papin, we have developed a new backend for ADA 2005. The mid-term project is to use tom-ADA to develop new optimisation phases of the GNAT-ADA compiler.

We have defined a new type system for Tom which allows to declare first-order signatures with subtyping. This is particularly useful to encode inheritance relations into algebraic terms. Considering Java as the host language, in [25] we present this type system with subtyping for Tom, that is compatible with Java's type system, and that performs both type checking and type inference. We propose an algorithm that checks if all patterns of a Tom program are well-typed. In addition, we propose an algorithm based on equality and subtyping constraints that infers types of variables occurring in a pattern. Both algorithms are exemplified and the proposed type system is showed to be sound and complete.

A first application consists in defining algebraic mappings for implementations of meta-models generated by the Eclipse Modeling Framework.